Nuprl Lemma : prime_imp_atomic 2,24
a:. prime(a)  atomic(a) 
latex

Definitionsprime(a), atomic(a), False, reducible(a), P & Q, A, a ~ b, P  Q, P  Q, Prop, b | a, x:A. B(x), t  T, x:A. B(x), , a  b, P  Q, P  Q, T, True
Lemmasmul com, true wf, squash wf, self divisor mul, assoced weakening, divides weakening, reducible wf, divides wf, assoced wf, not wf

origin